Okay. We are still looking at logic-based agents and we're kind of zooming in on a world

description language and the current proposal for a description language is...

Oh come on.

I'll have to get some chalk.

Good morning.

Could you give me a chalk?

Wonderful. All of mine have been stolen.

No, no, one is enough. Thank you.

So, remember we were looking at description logics which are somewhere between first-order logic and

propositional logic and below the decidability and undecidability line we have a logic called ALC

and that has the usual stuff we use for set descriptions, intersection, union, complement and a couple of others

but it actually introduces something which is a restricted quantification where R is a role

which just basically means binary relation, the father of relation, things like that.

And that, and of course there is another one which reads as the meaning of this is

the set of all objects X such that

all Y that are in R relation, that are R successors of X and X is in phi.

And with that we can express quite a lot.

In the beginning of last lecture I kind of made the observation that in natural languages if we have something like all

students sleep and first-order logic we might say for all X sleep of X implies that it sleeps.

The difference between first-order logic where quantification is unrestricted is in natural language we always have restricted

quantification which is kind of a step into the right direction and we can, in first-order logic we can mimic this

by this implication. That is if you want a hack, a hack around the fact that we have kind of unary quantification, unrestricted

we might have typed first-order logic where we could write something like for all X that are students

right, if you just tape type, sprinkle them over first-order logic that is something we can do, that is something often very very useful

and this in a way is much closer to that but you always have to kind of in advance choose whether student is a type or whether it's a predicate.

If I want to say something like all my children are students then I need it as a predicate and if I want to say all students sleep it must be a type

and you run into lots of problems that way and still different in ALC we don't have restrictions that are unary predicates or in other words just properties like being a student.

Here we have basically restrictions via relatedness, different mechanisms, you can kind of do the same thing and the role restriction is even more powerful

than the type restriction here, type first-order logic is undecidable whereas ALC as we've seen is decidable.

Okay and we did, come on move

We did a couple of examples, we looked at the semantics, we looked at the important thing here is we looked at an inference procedure.

As you say it, it's not true but an elaboration of that is true. It actually is decidable because you can always have finite models and in a way this calculus, the tableau calculus kind of gives you finite models.

You never have to consider infinite models, that gives you decidability.

And we even know, that was the last thing we did on Tuesday, we even know how big the things are by just looking at the formulae, input formulae.

We have a tableau calculus here where we're not actually talking about labelled formulae, labelled formulae as judgements about the truth of arbitrary formulae but here we have judgements of the form X is a member of C or X is related, is R related to Y.

Okay but still same idea, we have a closure rule, we have positive and negative AND rules and we have quantifier rules.

In the propositional tableau calculus we also had negation rules.

Why don't we have them here?

Why don't we need them?

That's something I didn't quite put emphasis on last time, we're only going to do this on negation normal form.

Which means negation only happens or complement only happen on atomic concepts.

Which means we never have to deal with it because we have exactly one rule that deals with them, namely this one.

With them, namely this one.

Okay so that's a little finicky thing, you should be aware of that.

I'm probably going to make the slides a bit better too when you're looking at this again somewhere end of March probably but you'll have the full idea.

We looked at termination by counting, we looked at a functional algorithm and then we realized that the algorithm for consistency was really not up to the real world.

In the real world we have concept axioms, we describe the world by axioms saying men and women are disjoint.

You either have a Y chromosome or you don't.

And without these axioms, especially disjointness axioms, we don't get very far.

We need to tell the system because it doesn't know that people are not chairs, that buildings are not people, that the number pi is not a fox or something like this.